\begin{tabbing}
precondition $a$: True
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=mk{-}ma(;\+
\\[0ex];
\\[0ex];
\\[0ex]$a$ : $\lambda$$s$,$v$. True;
\\[0ex];
\\[0ex];
\\[0ex];
\\[0ex];
\\[0ex];
\\[0ex];
\\[0ex])
\-
\end{tabbing}